Petri nets with inhibitor arcs are referred to as inhibitor-arc Petri nets. It is shown that modeling capability of inhibitor-arc Petri nets is equivalent to that of Turing machines. The subject of this paper is the legal firing sequence problem (INLFS) for inhibitor-arc Petri nets: given an inhibitor-arc Petri net IN, an initial marking M0 and a firing count vector X, find a firing sequence δ such that its firing starts from M0 and each transition t appears in δ exactly X(t) times as prescribed by X. The paper is the first step of research for time complexity analysis and designing algorithms of INLFS, one of the most fundamental problems for inhibitor-arc Petri nets having more modeling capability than ordinary Peri nets. The recognition version of INLFS, denoted as RINLFS, means a decision problem, asking a "yes" or "no" answer on the existence of a solution δ to INLFS. The main results are the following (1) and (2). (1) Proving (1-1) and (1-2) when the underlying Petri net of IN is an unweighted state machine: (1-1) INLFS can be solved in pseudo-polynomial (O(|X|)) time for IN of non-adjacent type having only one special place called a rivet; (1-2) RINLFS is NP-hard for IN with at least three rivets; (2) Proving that RINLFS for IN whose underlying Petri net is unweighted and forward conflict-free is NP-hard. Heuristic algorithms for solving INLFS are going to be proposed in separate papers.

The minimum initial marking problem MIM of Petri nets is described as follows: "Given a Petri net and a firing count vector X, find an initial marking M0, with the minimum total token number, for which there is a sequence δ of transitions such that each transition t appears exactly X(t) times in δ, the first transition is enabled at M0 and the rest can be fired one by one subsequently." This paper proposes two heuristic algorithms AAD and AMIM + and shows the following (1) and (2) through experimental results: (1) AAD is more capable than any other known algorithm; (2) AMIM + can produce M0, with a small number of tokens, even if other algorithms are too slow to compute M0 as the size of an input instance gets very large.

Petri nets are a well-known graphical and modeling tool for concurrent and distributed systems, and there have been many results on the theory, and also on practical applications. In the last decade, various Object-Oriented Petri nets (OO-nets) are proposed. As object orientation was adopted for programming languages, extension to OO-nets inspired from object-oriented programming is a natural flow. This article presents state-of-the-art on OO-nets.

This paper proposes a new change type for dynamic change of workflows, named Selective Shift. Workflow technology is being introduced in many companies. Workflows are business processes that allow for computerized support. The goal of workflow technology is to process workflow instances, called cases, as efficiently as possible. Companies need to change their workflows in order to adapt them to various requirements. Dynamic change is to change workflows having running cases. The most important issue in dynamic change is how running cases should be handled. Ellis et al. and Sadiq et al. have proposed change types that prescribe how to handle running cases. Their change types handle running cases collectively. If a change type can handle running cases separately, the change type would be more flexible and efficient than the conventional change types. However, there is no any change type that can handle running cases separately. Selective Shift to be proposed can handle running cases separately. We first present the concept and definition of Selective Shift. Then we give a method to handle running cases separately. Furthermore we give methods to handle running cases so that dynamic change becomes most efficient on one evaluation measure, called change time. Finally we compare Selective Shift with the conventional change types on change time by using 270 examples of dynamic change.

A siphon-trap(ST) of a Petri net N = (P,T,E,α,β) is defined as a set S of places such that, for any transition t, there is an edge from t to a place of S if and only if there is an edge from a place of S to t. A P-invariant is a |P|-dimensional vector Y with YtA = for the place-transition incidence matrix A of N. The Fourier-Motzkin method is well-known for computing all such invariants. This method, however, has a critical deficiency such that, even if a given Perti net N has any invariant, it is likely that no invariants are output because of memory overflow in storing intermediary vectors as candidates for invariants. In this paper, we propose an algorithm STFM_N for computing minimal-support nonnegative integer invariants: it tries to decrease the number of such candidate vectors in order to overcome this deficiency, by restricting computation of invariants to siphon-traps. It is shown, through experimental results, that STFM_N has high possibility of finding, if any, more minimal-support nonnegative integer invariants than any existing algorithm.

For fixed initial and destination states (i.e., markings), M0 and Md, there exist generally infinite firing count vectors in a Petri net. In this letter, it is shown that all fundamental particular solutions as well as all minimal T-invariants w.r.t. firing count vectors are needed to express an arbitrary firing count vector for the fixed M0 and Md. An algorithm for finding a special firing count vector which is expressed by using the only one specified fundamental particular solution is also given.

This paper proposes methods of computing maximum throughput for Petri nets that model workflows including resources, called WF-nets with resources. We first propose the formal definitions of WF-nets with resources and their subclasses: marked graph/state machine WF-nets with conflict-free resources (CF-Res-MG/SMWF-nets). We also show several properties of CF-Res-MG/SMWF-nets. Next we give the methods of computing maximum throughput for CF-Res-MG/SMWF-nets under condition that all tokens have to be processed in the order of First-In First-Out (FIFO). Concretely, for CF-Res-MGWF-nets, on the basis of Ramamoorthy's method of computing cycle time, we give an algorithm of computing maximum throughput under the FIFO condition. For CF-Res-SMWF-nets, there is not any method of computing maximum throughput under the FIFO condition. So we are the first to give an algorithm of computing maximum throughput for CF-Res-SMWF-nets under the FIFO condition. Finally we show an example of computing maximum throughput by using our method.

This paper addresses the scheduling problem of a class of automated manufacturing systems with multiple resource requests. In the automated manufacturing system model, a set of jobs is to be processed and each job requires a sequence of operations. Each operation may need more than one resource type and multiple identical units with the same resource type. Upon the completion of an operation, resources needed in the next operation of the same job cannot be released and the remaining resources cannot be released until the start of the next operation. The scheduling problem is formulated by Timed Petri nets model under which the scheduling goal consists in sequencing the transition firing sequence in order to avoid the deadlock situation and to minimize the makespan. In the proposed genetic algorithm with deadlock-free constraint, Petri net transition sequence is coded and a deadlock detection method based on D-siphon technology is proposed to reschedule the sequence of transitions. The enabled transitions should be fired as early as possible and thus the quality of solutions can be improved. In the fitness computation procedure, a penalty item for the infeasible solution is involved to prevent the search process from converging to the infeasible solution. The method proposed in this paper can get a feasible scheduling strategy as well as enable the system to achieve good performance. Numerical results presented in the paper show the efficiency of the proposed algorithm.

Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.

This paper discusses formal modeling and performance evaluation for a type of dynamic change of workflow, called Migrate. Workflow means the flow of work and is designed to process similar instances, called cases. Companies need to continuously refine their current workflow in order to adapt them to various requirements. The change of a current workflow is called dynamic change of the workflow. Before changing a workflow, there exist cases in the workflow. If these cases are ignored or fall into deadlock, the changed workflow would become inconsistent. Since Ellis et al. proposed three change types, Flush, Abort, and Synthetic Cut-Over that keep consistency of workflows in 1995, various change types have been proposed, in which there is a promising change type called Migrate that is proposed by Sadiq et al. Sadiq et al. proposed the concept of Migrate, but did not give a formal model of Migrate. Meanwhile, we have proposed a measure, called change time, in order to evaluate dynamic change of workflows, and used this measure to evaluate the performance on change time for Ellis et al. 's three change types. However, the performance evaluation on change time for Migrate has not been done. In this paper, we first give a Petri-nets-based model of Migrate. Then we present a method of computing change time based on the net model. Finally, we apply the method to 270 examples and show the comparison results between Migrate and Ellis et al. 's three change types.

This paper develops a framework to support trace theoretic verification of timed circuits and systems. A theoretical foundation for classifying timed traces as either successes or failures is developed. The concept of the semimirror is introduced to allow conformance checking thus supporting hierarchical verification of timed circuits and systems. Finally, we relate our framework to those previously proposed for timing verification.

In this paper, new integrated schemes of scheduling real-time traffic and cell loss control in high speed ATM networks are proposed for multiple priorities based on variable queue length thresholds for scheduling and the Partial Buffer Sharing policy for cell loss control. In our schemes, the queues for buffering arriving cells can be constructed in two ways: one individual queue for each user connection, or one physical queue for all user connections. The proposed schemes are considered to provide guaranteed QoS for each connection and cell sequence integrity for virtual channel/path characteristics. Moreover, these new schemes are quite flexible and can realize different scheduling algorithms. This paper also provides the Stochastic Petri Net models of these integrated schemes and an approximate analysis technique, which significantly reduces the complexity of the model solution and can be applied to real ATM switch models. From the numerical results, we can see that our schemes outperform those well-known schemes such as the head-of-line (HOL) priority control and the queue length threshold (QLT) policy.

Adaptation of software components to the requirements is one of the key concerns in Component Based Software Development (CBSD). In this paper, we propose a formal approach to compose component based systems which are adaptable to the requirements. We focus on the functional aspects of software components and requirements, which are expressed in S-sorted functions. Those S-sorted functions are transformed into Colored Petri Nets (CPN) models in order to evaluate connectivity between the components, and to evaluate adaptability of composed systems to the requirements. The connectivity is measured based on colors or data types in CPN, while the adaptability is measured based on functional equivalency. We introduce simple glue codes to connect the components each other. The paper focuses on business applications, however the proposed approach can be applied to any other domains as far as the functional adaptability is concerned.

It is one of the difficulties in enterprise modeling that we must deal with many fragmented pieces of knowledge provided by various domain-experts, which are usually based on mutually different viewpoints of them. This paper presents a formal approach to integrate those pieces into enterprise-wide model units using Rough Set Theory (RST). We focus on business processes in order to recognize and identify the constituents or units of enterprise models, which would compose the model expressing the various aspects of the enterprise. We defined five model unit types of "resource," "organization," "task," "function," and "behavior. " The first three types represent the static aspect of the enterprise, whereas the last two types represent the dynamic aspect of it. Those units are initially elicited from each domain-expert as his/her own individual model units, then they are integrated into enterprise-wide units using RST. Our approach is methodology-free, and any methodologies can include it in their early stage to identify what composes the enterprise.

Despite their attractive properties, networked virtual environments (net-VEs) are notoriously difficult to design, implement and test due to the concurrency, real-time and networking features in these systems. The current practice for net-VE design is basically trial and error, empirical, and totally lacks formal methods. This paper proposes to apply a Petri net formal modeling technique to a net-VE: NICE (Narrative Immersive Constructionist/Collaborative Environment), predict the net-VE performance based on simulation, and improve the net-VE performance. NICE is essentially a network of collaborative virtual reality systems called CAVE-(CAVE Automatic Virtual Environment). First, we present extended fuzzy-timing Petri net models of both CAVE and NICE. Then, by using these models and Design/CPN as the simulation tool, we have conducted various simulations to study real-time behavior, network effects and performance (latencies and jitters) of NICE. Our simulation results are consistent with experimental data.

Generating state spaces is one of important and general methods in the analysis of Petri nets. There are two reasons why state spaces of Petri nets become so large. One is concurrent occurring of transitions, and the other is periodic occurring of firing sequences. This paper focuses on the second problem, and proposes a new algorithm for exploring state spaces of finite capacity Petri nets with large capacities. In the proposed algorithm, the state space is represented in the form of a tree such that a set of markings generated by periodic occurrences of firing sequences is associated with each node, and it is much smaller than the reachability graph.

In computer science, concepts of resource such as data consumption and of time such as execution time are very important. Logical systems which can treat them have been applied in that field. Linear logic has been called a resource conscious logic. The expressive power is enough to describe a dynamic change in process environments. However, linear logic is not enough to treat a dynamic change in environments with the passage of time since it does not include a concept of time directly. A typical example is the relation between linear logic and Petri nets. It is well known that the reachability problem for Petri nets is equivalent to the provability for the corresponding sequent of linear logic. But linear logic cannot naturally represent timed Petri nets which are extensions of ordinary Petri nets with respect to time concept. So we extend linear logic with respect to time concept in order to introduce a resource-conscious and time-dependent logical system, that is, temporal linear logic. This system has some temporal operators "" which means a resource usable only once at the next time, "" which means a resource usable only once at anytime, and a modal storage operator "!" which means a resource usable any times at anytime. We can show that the reachability problem for timed Petri nets is equivalent to the provability for the corresponding sequent of temporal linear logic. In this paper, we also represent the description of synchronous communication model by temporal linear logic. The expressive power of temporal linear logic will be applicable to various fields of computer science.

We determine the optimum time TOPT to order a spare part for a system before the part in operation has failed. TOPT is a function of the part's failure-time distribution, the lead (delivery) time of the part, its inventory cost, and the cost of downtime while waiting delivery. The probabilities of the system's up and down states are obtained from a non-regenerative stochastic Petri net. TOPT is found by minimizing E[cost], the expected cost of inventory and downtime. Three cases are compared: 1) Exponential order and lead times, 2) Deterministic order time and exponential lead time, and 3) Deterministic order and lead times. In Case 1, it is shown analytically that, depending on the ratio of inventory to downtime costs, the optimum policy is one of three: order a spare part immediately at t = 0, wait until the part in operation fails, or order before failure at TOPT > 0. Numerical examples illustrate the three cases.

This paper considers two simulation models for simple unreliable file systems with checkpointing and rollback recovery. In Model 1, the checkpoint is generated at a pre-specified time and the information on the main memory since the last checkpoint is back-uped in a secondary medium. On the other hand, in Model 2, the checkpointing is executed at the time when the number of transactions completed for processing is achieved at a pre-determined level. However, it is difficult to treat such models analytically without employing any approximation method, if queueing effects related with arrival and processing of transactions can not be ignored. We apply the generalized stochastic Petri net (GSPN) to represent the stochastic behaviour of systems under two checkpointing schemes. Throughout GSPN simulation, we evaluate quantitatively the maintainability of checkpoint models under consideration and examine the dependence of model parameters in the optimal checkpoint policies and their associated system availabilities.

Software Composition is one of the major concerns in component based software development (CBSD). In this paper, we present a formal approach to construct software systems from requirements models using available components. We focus on the knowledge resides in the requirements and the components in order to deal with those heterogeneous concepts. This approach consists of three steps. The first step is selecting adaptable components to the requirements model. The requirements and the components are transformed into the form of Σ algebra, and the component adaptability is evaluated by Σ homomorphism. Rough Set Theory (RST) is used to make carriers of two Σ algebras common, which are derived from the requirements and the components. The second step is identifying the control structure of the requirements. Decision tables are used for representing the knowledge on the requirements, and RST is used to optimize the control structure. The third step is to implement the control structure as glue codes which would perform the components appropriately. This approach mainly focuses on enterprise back-office applications in this paper, however, it can be easily applied to other domains, since it assumes the requirements to be expressed in Colored Petri Nets (CPN), and CPN can express various problem domains other than enterprise back-office applications.